Skolem Normal Form

释义 Definition（中文）

Skolem normal form（斯科勒姆范式）是一阶逻辑中一种标准化的公式形式：通过Skolem 化（Skolemization）消去存在量词，用Skolem 函数/常元来替代被存在量词约束的变量，最终把公式改写成形如
∀x₁…∀xₙ φ 的形式，其中 φ 不再含有存在量词（但会包含新引入的 Skolem 函数或常元）。
常用于自动定理证明、可满足性与推理算法中。（不同教材对细节表述略有差异；有时会进一步要求矩阵部分满足特定的子句形态。）

发音 Pronunciation（IPA）

/ˈskuːləm ˈnɔːrməl fɔːrm/

例句 Examples（EN/中文）

We first convert the formula to Skolem normal form before applying resolution.
我们先把公式转换成斯科勒姆范式，再应用归结法。

After prenexing, Skolemization replaces each existential variable with a Skolem function of the preceding universal variables, yielding a Skolem normal form that preserves satisfiability.
在前束化之后，Skolem 化会把每个存在变量替换为以前面的全称变量为自变量的 Skolem 函数，从而得到保持可满足性的斯科勒姆范式。

词源 Etymology（中文）

“Skolem”来自挪威逻辑学家 Thoralf Skolem（托拉尔夫·斯科勒姆）的姓氏；“normal form”意为“规范形式/标准形式”。该术语与Skolem 化相关，用于把一阶逻辑公式转成更便于机器推理处理的标准结构。

相关词 Related Words

• Prenex Normal Form
• Skolemization
• Herbrand Theorem
• First-Order Logic
• Quantifier
• Universal Quantifier
• Existential Quantifier
• Satisfiability
• Resolution
• Conjunctive Normal Form

文学与名著中的出现 Literary Works（举例）

• Herbert B. Enderton，《A Mathematical Introduction to Logic》：在一阶逻辑标准化与可满足性讨论中介绍 Skolem 化与相应的规范形式。
• Elliott Mendelson，《Introduction to Mathematical Logic》：在量词处理、Skolem 化与模型论相关章节中出现。
• Joseph R. Shoenfield，《Mathematical Logic》：涉及 Skolem 函数、Skolem 化与规范形式的推导。
• Raymond M. Smullyan，《First-Order Logic》：与前束范式、子句化、证明程序相关处常用到该概念。
• Chang & Keisler，《Model Theory》：在模型论背景下讨论 Skolem 函数与相关标准化思想（术语出现依版本与章节而定）。